/*
 * Copyright 2011, 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.combinatorial.solver;

import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePatternFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree.NotSymmetricException;
import de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree.SplittingTree;
import de.wenzelmf.booleanFunction.lpb.util.ConversionException;
import de.wenzelmf.booleanFunction.lpb.util.DNFToLPB;
import de.wenzelmf.booleanFunction.lpb.util.LPB;
import de.wenzelmf.booleanFunction.lpb.util.LPBCombinatorialConstants;

/**
 * This class is a bridge that brings together the {@link DNFToLPB} interface with the
 * {@link TreeToLPB} interface.
 * 
 * This class therefore overwrites the {@code convert} method of the {@link DNFToLPB} interface.
 * It tries to create a splitting tree from the DNF and uses the {@link TreeToLPB#solve(SplittingTree)}
 * method to create a LPB.
 * 
 * All constructs without the value {@code releaseMemory} will set this value to {@code true}.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class TreeSolver implements DNFToLPB
{

	/**
	 * {@code true} if a symmetry test should be applied while creating the tree.
	 */
	private boolean symmetryTest;
	/**
	 * The occurrence pattern factory that is used to create the occurrence patterns (required
	 * to create the splitting tree).
	 */
	private OccurrencePatternFactory opFactory;
	/**
	 * Clause factory that is used to create the clauses DNFs in the splitting tree.
	 */
	private ClauseFactory clauseFactory;
	/**
	 * DNF factory that is used to create the DNFs of the splitting tree.
	 */
	private DNFFactory dnfFactory;
	/**
	 * The solver that accepts a splitting tree and returns a LPB.
	 */
	private TreeToLPB solver;
	/**
	 * The number of columns in the table (just for efficiency reasons), a negative value indicates
	 * that the value is unknown.
	 */
	private int columns;
	/**
	 * This value is true if the DNFs and occurrence patterns of the splitting tree should be destroyed.
	 */
	private boolean releaseMemory;
	
	public TreeSolver(boolean symmetryTest, OccurrencePatternFactory opFactory, 
			ClauseFactory clauseFactory, DNFFactory dnfFactory, TreeToLPB solver, int columns,
			boolean releaseMemory)
	{
		this.symmetryTest = symmetryTest;
		this.opFactory = opFactory;
		this.solver = solver;
		this.clauseFactory = clauseFactory;
		this.dnfFactory = dnfFactory;
		this.columns = columns;
		this.releaseMemory = releaseMemory;
	}
	
	/**
	 * Constructs a new TreeSolver.
	 * 
	 * @param symmetryTest {@code true} if a symmetry test should be applied while creating the tree.
	 * @param opFactory The occurrence pattern factory that is used to create the occurrence patterns (required
	 * to create the splitting tree).
	 * @param clauseFactory Clause factory that is used to create the clauses DNFs in the splitting tree.
	 * @param dnfFactory DNF factory that is used to create the DNFs of the splitting tree.
	 * @param solver The solver that accepts a splitting tree and returns a LPB.
	 * @param columns The number of columns in the table (just for efficiency reasons), a negative value indicates
	 * that the value is unknown.
	 */
	public TreeSolver(boolean symmetryTest, OccurrencePatternFactory opFactory, 
			ClauseFactory clauseFactory, DNFFactory dnfFactory, TreeToLPB solver, int columns)
	{
		this(symmetryTest, opFactory, clauseFactory, dnfFactory, solver, columns, true);
	}
	
	/**
	 * Constructs a new TreeSolver.
	 * 
	 * @param symmetryTest {@code true} if a symmetry test should be applied while creating the tree.
	 * @param opFactory The occurrence pattern factory that is used to create the occurrence patterns (required
	 * to create the splitting tree).
	 * @param clauseFactory Clause factory that is used to create the clauses DNFs in the splitting tree.
	 * @param dnfFactory DNF factory that is used to create the DNFs of the splitting tree.
	 * @param solver The solver that accepts a splitting tree and returns a LPB.
	 */
	public TreeSolver(boolean symmetryTest, OccurrencePatternFactory opFactory, 
			ClauseFactory clauseFactory, DNFFactory dnfFactory, TreeToLPB solver)
	{
		this(symmetryTest, opFactory, clauseFactory, dnfFactory, solver, -1);
	}
	
	/**
	 * Creates a new TreeSolver with default factories defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest {@code true} if a symmetry test should be applied while creating the tree.
	 * @param solver The solver that accepts a splitting tree and returns a LPB.
	 * @param columns The number of columns in the table (just for efficiency reasons), a negative value indicates
	 * that the value is unknown.
	 * 
	 * @see #TreeSolver(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, TreeToLPB, int)
	 */
	public TreeSolver(boolean symmetryTest, TreeToLPB solver, int columns)
	{
		this(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, LPBCombinatorialConstants.defaultClauseFactory,
				LPBCombinatorialConstants.defaultDNFFactory, solver, columns);
	}
	
	/**
	 * Creates a new TreeSolver with default factories defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest {@code true} if a symmetry test should be applied while creating the tree.
	 * @param solver The solver that accepts a splitting tree and returns a LPB.
	 * 
	 * @see #TreeSolver(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, TreeToLPB)
	 */
	public TreeSolver(boolean symmetryTest, TreeToLPB solver)
	{
		this(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, LPBCombinatorialConstants.defaultClauseFactory,
				LPBCombinatorialConstants.defaultDNFFactory, solver);
	}
	
	/**
	 * Method used to convert a DNF to a LPB.
	 * 
	 * This method first creates the splitting tree for &Phi; and then tries to generate a LPB
	 * using the {@link TreeToLPB#solve(SplittingTree)} method.
	 * 
	 * @throws ConversionException If a {@link NotSymmetricException} is thrown or a
	 * {@link ConversionException} is thrown by the solver.
	 */
	@Override
	public LPB convert(DNF phi) throws ConversionException
	{
		SplittingTree t;
		if(columns < 0)
		{
			t = new SplittingTree(phi, opFactory);
		}
		else
		{
			t = new SplittingTree(phi, columns, opFactory);
		}
		try
		{
			t.createTree(symmetryTest, opFactory, clauseFactory, dnfFactory, releaseMemory);
		}
		catch(NotSymmetricException e)
		{
			throw new ConversionException(e);
		}
		return solver.solve(t);
	}
	
	/**
	 * Method used to convert a DNF to a LPB.
	 * 
	 * This method first creates the splitting tree for &Phi; and uses the synchronized version
	 * of createTree ({@link SplittingTree#createTreeSynchronized(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}).
	 * and then tries to generate a LPB using the {@link TreeToLPB#solve(SplittingTree)} method.
	 * 
	 * @throws ConversionException If a {@link NotSymmetricException} is thrown or a
	 * {@link ConversionException} is thrown by the solver.
	 * @throws InterruptedException If another thread has interrupted one of the threads.
	 */
	public LPB convertSynchronized(DNF phi) throws ConversionException, InterruptedException
	{
		SplittingTree t;
		if(columns < 0)
		{
			t = new SplittingTree(phi, opFactory);
		}
		else
		{
			t = new SplittingTree(phi, columns, opFactory);
		}
		try
		{
			t.createTreeSynchronized(symmetryTest, opFactory, clauseFactory, dnfFactory, releaseMemory);
		}
		catch(NotSymmetricException e)
		{
			throw new ConversionException(e);
		}
		return solver.solve(t);
	}
	
	/**
	 * Method used to convert a DNF to a LPB.
	 * 
	 * This method first creates the splitting tree for &Phi; using the
	 * {@link SplittingTree#createTreeDepthFirst(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * method and then tries to generate a LPB using the {@link TreeToLPB#solve(SplittingTree)} method.
	 * 
	 * @throws ConversionException If a {@link NotSymmetricException} is thrown or a
	 * {@link ConversionException} is thrown by the solver.
	 */
	public LPB convertDepthFirst(DNF phi) throws ConversionException
	{
		SplittingTree t;
		if(columns < 0)
		{
			t = new SplittingTree(phi, opFactory);
		}
		else
		{
			t = new SplittingTree(phi, columns, opFactory);
		}
		try
		{
			t.createTreeDepthFirst(symmetryTest, opFactory, clauseFactory, dnfFactory, releaseMemory);
		}
		catch(NotSymmetricException e)
		{
			throw new ConversionException(e);
		}
		return solver.solve(t);
	}

}
